
; Copyright (c) 2015 Microsoft Corporation
;; NOTE: we disable model validation in this example because
;; we don't store the interpretation of division by 0 produced by
;; Z3. So, the model validation will fail when a division by 0 is found
(set-option :model-validate false)

(set-option :auto-config true)
(set-option :rewriter.hi-div0 true)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 8) (_ BitVec 6) (_ BitVec 2)) (_ BitVec 7))
(declare-fun p0 ( (_ BitVec 2)) Bool)
(declare-fun v0 () (_ BitVec 15))
(declare-fun v1 () (_ BitVec 10))
(declare-fun v2 () (_ BitVec 1))
(declare-fun v3 () (_ BitVec 12))
(assert (let ((e4(_ bv39 7)))
(let ((e5 (f0 ((_ sign_extend 7) v2) ((_ sign_extend 5) v2) ((_ zero_extend 1) v2))))
(let ((e6 (ite (p0 ((_ extract 6 5) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e7 (bvurem ((_ zero_extend 11) e6) v3)))
(let ((e8 ((_ rotate_left 0) v2)))
(let ((e9 (bvxor ((_ zero_extend 5) e5) v3)))
(let ((e10 (bvlshr ((_ sign_extend 6) v2) e5)))
(let ((e11 (ite (bvslt e5 ((_ sign_extend 6) e6)) (_ bv1 1) (_ bv0 1))))
(let ((e12 (ite (bvsgt ((_ sign_extend 8) e10) v0) (_ bv1 1) (_ bv0 1))))
(let ((e13 (bvor v1 ((_ sign_extend 9) e11))))
(let ((e14 (bvshl v0 ((_ zero_extend 3) e9))))
(let ((e15 (bvadd ((_ zero_extend 2) e13) e7)))
(let ((e16 (bvurem ((_ zero_extend 11) v2) e15)))
(let ((e17 (ite (bvslt v0 ((_ sign_extend 3) e9)) (_ bv1 1) (_ bv0 1))))
(let ((e18 (ite (bvuge e5 e4) (_ bv1 1) (_ bv0 1))))
(let ((e19 (p0 ((_ extract 6 5) e10))))
(let ((e20 (bvuge ((_ zero_extend 5) v1) v0)))
(let ((e21 (bvslt e16 ((_ sign_extend 5) e10))))
(let ((e22 (bvsgt ((_ sign_extend 5) e10) e16)))
(let ((e23 (bvsle ((_ zero_extend 11) e8) e7)))
(let ((e24 (= ((_ zero_extend 5) e10) e7)))
(let ((e25 (bvuge ((_ sign_extend 6) e18) e4)))
(let ((e26 (distinct v3 ((_ zero_extend 2) v1))))
(let ((e27 (bvule e6 e17)))
(let ((e28 (p0 ((_ sign_extend 1) e6))))
(let ((e29 (bvuge ((_ sign_extend 6) e18) e5)))
(let ((e30 (bvuge e8 e6)))
(let ((e31 (distinct e15 ((_ sign_extend 11) e11))))
(let ((e32 (bvule ((_ sign_extend 11) e6) e16)))
(let ((e33 (bvule ((_ zero_extend 6) e11) e4)))
(let ((e34 (bvsle v3 v3)))
(let ((e35 (bvsgt ((_ zero_extend 11) e6) e16)))
(let ((e36 (bvule ((_ sign_extend 11) e11) v3)))
(let ((e37 (bvuge e14 ((_ zero_extend 3) e16))))
(let ((e38 (= ((_ sign_extend 3) e15) v0)))
(let ((e39 (bvsgt e11 e11)))
(let ((e40 (bvsge e18 e18)))
(let ((e41 (distinct e17 e11)))
(let ((e42 (p0 ((_ extract 4 3) e10))))
(let ((e43 (p0 ((_ extract 1 0) e10))))
(let ((e44 (bvult v0 ((_ zero_extend 14) e18))))
(let ((e45 (p0 ((_ extract 10 9) v3))))
(let ((e46 (bvuge e9 ((_ zero_extend 5) e10))))
(let ((e47 (bvsge v3 ((_ sign_extend 11) e6))))
(let ((e48 (bvslt v3 ((_ sign_extend 5) e4))))
(let ((e49 (bvsge e18 e17)))
(let ((e50 (bvult e15 ((_ sign_extend 5) e10))))
(let ((e51 (bvslt ((_ zero_extend 9) v2) v1)))
(let ((e52 (bvsge ((_ sign_extend 11) e8) v3)))
(let ((e53 (= ((_ zero_extend 11) e17) e9)))
(let ((e54 (bvsle ((_ sign_extend 11) e12) e16)))
(let ((e55 (bvslt e15 ((_ zero_extend 11) v2))))
(let ((e56 (bvule v2 e17)))
(let ((e57 (bvugt ((_ zero_extend 9) v2) e13)))
(let ((e58 (xor e47 e50)))
(let ((e59 (not e26)))
(let ((e60 (= e51 e44)))
(let ((e61 (= e37 e36)))
(let ((e62 (not e29)))
(let ((e63 (ite e41 e30 e32)))
(let ((e64 (= e40 e46)))
(let ((e65 (xor e55 e35)))
(let ((e66 (= e60 e59)))
(let ((e67 (ite e62 e38 e19)))
(let ((e68 (ite e34 e61 e66)))
(let ((e69 (and e27 e43)))
(let ((e70 (and e53 e48)))
(let ((e71 (xor e25 e69)))
(let ((e72 (not e31)))
(let ((e73 (and e72 e65)))
(let ((e74 (=> e71 e54)))
(let ((e75 (=> e42 e58)))
(let ((e76 (= e33 e56)))
(let ((e77 (= e45 e49)))
(let ((e78 (not e39)))
(let ((e79 (= e63 e28)))
(let ((e80 (or e52 e75)))
(let ((e81 (not e57)))
(let ((e82 (ite e22 e78 e79)))
(let ((e83 (not e68)))
(let ((e84 (and e82 e83)))
(let ((e85 (or e77 e20)))
(let ((e86 (and e24 e76)))
(let ((e87 (=> e23 e74)))
(let ((e88 (xor e67 e67)))
(let ((e89 (xor e64 e21)))
(let ((e90 (not e73)))
(let ((e91 (ite e70 e90 e88)))
(let ((e92 (xor e81 e91)))
(let ((e93 (=> e80 e80)))
(let ((e94 (not e86)))
(let ((e95 (not e84)))
(let ((e96 (xor e92 e94)))
(let ((e97 (=> e93 e96)))
(let ((e98 (ite e97 e89 e89)))
(let ((e99 (not e87)))
(let ((e100 (and e98 e85)))
(let ((e101 (=> e100 e100)))
(let ((e102 (or e99 e99)))
(let ((e103 (and e95 e101)))
(let ((e104 (= e103 e103)))
(let ((e105 (or e104 e104)))
(let ((e106 (= e105 e102)))
e106
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

(reset)
(set-option :auto-config true)
(set-option :rewriter.hi-div0 false)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 8) (_ BitVec 6) (_ BitVec 2)) (_ BitVec 7))
(declare-fun p0 ( (_ BitVec 2)) Bool)
(declare-fun v0 () (_ BitVec 15))
(declare-fun v1 () (_ BitVec 10))
(declare-fun v2 () (_ BitVec 1))
(declare-fun v3 () (_ BitVec 12))
(assert (let ((e4(_ bv39 7)))
(let ((e5 (f0 ((_ sign_extend 7) v2) ((_ sign_extend 5) v2) ((_ zero_extend 1) v2))))
(let ((e6 (ite (p0 ((_ extract 6 5) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e7 (bvurem ((_ zero_extend 11) e6) v3)))
(let ((e8 ((_ rotate_left 0) v2)))
(let ((e9 (bvxor ((_ zero_extend 5) e5) v3)))
(let ((e10 (bvlshr ((_ sign_extend 6) v2) e5)))
(let ((e11 (ite (bvslt e5 ((_ sign_extend 6) e6)) (_ bv1 1) (_ bv0 1))))
(let ((e12 (ite (bvsgt ((_ sign_extend 8) e10) v0) (_ bv1 1) (_ bv0 1))))
(let ((e13 (bvor v1 ((_ sign_extend 9) e11))))
(let ((e14 (bvshl v0 ((_ zero_extend 3) e9))))
(let ((e15 (bvadd ((_ zero_extend 2) e13) e7)))
(let ((e16 (bvurem ((_ zero_extend 11) v2) e15)))
(let ((e17 (ite (bvslt v0 ((_ sign_extend 3) e9)) (_ bv1 1) (_ bv0 1))))
(let ((e18 (ite (bvuge e5 e4) (_ bv1 1) (_ bv0 1))))
(let ((e19 (p0 ((_ extract 6 5) e10))))
(let ((e20 (bvuge ((_ zero_extend 5) v1) v0)))
(let ((e21 (bvslt e16 ((_ sign_extend 5) e10))))
(let ((e22 (bvsgt ((_ sign_extend 5) e10) e16)))
(let ((e23 (bvsle ((_ zero_extend 11) e8) e7)))
(let ((e24 (= ((_ zero_extend 5) e10) e7)))
(let ((e25 (bvuge ((_ sign_extend 6) e18) e4)))
(let ((e26 (distinct v3 ((_ zero_extend 2) v1))))
(let ((e27 (bvule e6 e17)))
(let ((e28 (p0 ((_ sign_extend 1) e6))))
(let ((e29 (bvuge ((_ sign_extend 6) e18) e5)))
(let ((e30 (bvuge e8 e6)))
(let ((e31 (distinct e15 ((_ sign_extend 11) e11))))
(let ((e32 (bvule ((_ sign_extend 11) e6) e16)))
(let ((e33 (bvule ((_ zero_extend 6) e11) e4)))
(let ((e34 (bvsle v3 v3)))
(let ((e35 (bvsgt ((_ zero_extend 11) e6) e16)))
(let ((e36 (bvule ((_ sign_extend 11) e11) v3)))
(let ((e37 (bvuge e14 ((_ zero_extend 3) e16))))
(let ((e38 (= ((_ sign_extend 3) e15) v0)))
(let ((e39 (bvsgt e11 e11)))
(let ((e40 (bvsge e18 e18)))
(let ((e41 (distinct e17 e11)))
(let ((e42 (p0 ((_ extract 4 3) e10))))
(let ((e43 (p0 ((_ extract 1 0) e10))))
(let ((e44 (bvult v0 ((_ zero_extend 14) e18))))
(let ((e45 (p0 ((_ extract 10 9) v3))))
(let ((e46 (bvuge e9 ((_ zero_extend 5) e10))))
(let ((e47 (bvsge v3 ((_ sign_extend 11) e6))))
(let ((e48 (bvslt v3 ((_ sign_extend 5) e4))))
(let ((e49 (bvsge e18 e17)))
(let ((e50 (bvult e15 ((_ sign_extend 5) e10))))
(let ((e51 (bvslt ((_ zero_extend 9) v2) v1)))
(let ((e52 (bvsge ((_ sign_extend 11) e8) v3)))
(let ((e53 (= ((_ zero_extend 11) e17) e9)))
(let ((e54 (bvsle ((_ sign_extend 11) e12) e16)))
(let ((e55 (bvslt e15 ((_ zero_extend 11) v2))))
(let ((e56 (bvule v2 e17)))
(let ((e57 (bvugt ((_ zero_extend 9) v2) e13)))
(let ((e58 (xor e47 e50)))
(let ((e59 (not e26)))
(let ((e60 (= e51 e44)))
(let ((e61 (= e37 e36)))
(let ((e62 (not e29)))
(let ((e63 (ite e41 e30 e32)))
(let ((e64 (= e40 e46)))
(let ((e65 (xor e55 e35)))
(let ((e66 (= e60 e59)))
(let ((e67 (ite e62 e38 e19)))
(let ((e68 (ite e34 e61 e66)))
(let ((e69 (and e27 e43)))
(let ((e70 (and e53 e48)))
(let ((e71 (xor e25 e69)))
(let ((e72 (not e31)))
(let ((e73 (and e72 e65)))
(let ((e74 (=> e71 e54)))
(let ((e75 (=> e42 e58)))
(let ((e76 (= e33 e56)))
(let ((e77 (= e45 e49)))
(let ((e78 (not e39)))
(let ((e79 (= e63 e28)))
(let ((e80 (or e52 e75)))
(let ((e81 (not e57)))
(let ((e82 (ite e22 e78 e79)))
(let ((e83 (not e68)))
(let ((e84 (and e82 e83)))
(let ((e85 (or e77 e20)))
(let ((e86 (and e24 e76)))
(let ((e87 (=> e23 e74)))
(let ((e88 (xor e67 e67)))
(let ((e89 (xor e64 e21)))
(let ((e90 (not e73)))
(let ((e91 (ite e70 e90 e88)))
(let ((e92 (xor e81 e91)))
(let ((e93 (=> e80 e80)))
(let ((e94 (not e86)))
(let ((e95 (not e84)))
(let ((e96 (xor e92 e94)))
(let ((e97 (=> e93 e96)))
(let ((e98 (ite e97 e89 e89)))
(let ((e99 (not e87)))
(let ((e100 (and e98 e85)))
(let ((e101 (=> e100 e100)))
(let ((e102 (or e99 e99)))
(let ((e103 (and e95 e101)))
(let ((e104 (= e103 e103)))
(let ((e105 (or e104 e104)))
(let ((e106 (= e105 e102)))
e106
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)


(reset)
(set-option :auto-config false)
(set-option :rewriter.hi-div0 true)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 8) (_ BitVec 6) (_ BitVec 2)) (_ BitVec 7))
(declare-fun p0 ( (_ BitVec 2)) Bool)
(declare-fun v0 () (_ BitVec 15))
(declare-fun v1 () (_ BitVec 10))
(declare-fun v2 () (_ BitVec 1))
(declare-fun v3 () (_ BitVec 12))
(assert (let ((e4(_ bv39 7)))
(let ((e5 (f0 ((_ sign_extend 7) v2) ((_ sign_extend 5) v2) ((_ zero_extend 1) v2))))
(let ((e6 (ite (p0 ((_ extract 6 5) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e7 (bvurem ((_ zero_extend 11) e6) v3)))
(let ((e8 ((_ rotate_left 0) v2)))
(let ((e9 (bvxor ((_ zero_extend 5) e5) v3)))
(let ((e10 (bvlshr ((_ sign_extend 6) v2) e5)))
(let ((e11 (ite (bvslt e5 ((_ sign_extend 6) e6)) (_ bv1 1) (_ bv0 1))))
(let ((e12 (ite (bvsgt ((_ sign_extend 8) e10) v0) (_ bv1 1) (_ bv0 1))))
(let ((e13 (bvor v1 ((_ sign_extend 9) e11))))
(let ((e14 (bvshl v0 ((_ zero_extend 3) e9))))
(let ((e15 (bvadd ((_ zero_extend 2) e13) e7)))
(let ((e16 (bvurem ((_ zero_extend 11) v2) e15)))
(let ((e17 (ite (bvslt v0 ((_ sign_extend 3) e9)) (_ bv1 1) (_ bv0 1))))
(let ((e18 (ite (bvuge e5 e4) (_ bv1 1) (_ bv0 1))))
(let ((e19 (p0 ((_ extract 6 5) e10))))
(let ((e20 (bvuge ((_ zero_extend 5) v1) v0)))
(let ((e21 (bvslt e16 ((_ sign_extend 5) e10))))
(let ((e22 (bvsgt ((_ sign_extend 5) e10) e16)))
(let ((e23 (bvsle ((_ zero_extend 11) e8) e7)))
(let ((e24 (= ((_ zero_extend 5) e10) e7)))
(let ((e25 (bvuge ((_ sign_extend 6) e18) e4)))
(let ((e26 (distinct v3 ((_ zero_extend 2) v1))))
(let ((e27 (bvule e6 e17)))
(let ((e28 (p0 ((_ sign_extend 1) e6))))
(let ((e29 (bvuge ((_ sign_extend 6) e18) e5)))
(let ((e30 (bvuge e8 e6)))
(let ((e31 (distinct e15 ((_ sign_extend 11) e11))))
(let ((e32 (bvule ((_ sign_extend 11) e6) e16)))
(let ((e33 (bvule ((_ zero_extend 6) e11) e4)))
(let ((e34 (bvsle v3 v3)))
(let ((e35 (bvsgt ((_ zero_extend 11) e6) e16)))
(let ((e36 (bvule ((_ sign_extend 11) e11) v3)))
(let ((e37 (bvuge e14 ((_ zero_extend 3) e16))))
(let ((e38 (= ((_ sign_extend 3) e15) v0)))
(let ((e39 (bvsgt e11 e11)))
(let ((e40 (bvsge e18 e18)))
(let ((e41 (distinct e17 e11)))
(let ((e42 (p0 ((_ extract 4 3) e10))))
(let ((e43 (p0 ((_ extract 1 0) e10))))
(let ((e44 (bvult v0 ((_ zero_extend 14) e18))))
(let ((e45 (p0 ((_ extract 10 9) v3))))
(let ((e46 (bvuge e9 ((_ zero_extend 5) e10))))
(let ((e47 (bvsge v3 ((_ sign_extend 11) e6))))
(let ((e48 (bvslt v3 ((_ sign_extend 5) e4))))
(let ((e49 (bvsge e18 e17)))
(let ((e50 (bvult e15 ((_ sign_extend 5) e10))))
(let ((e51 (bvslt ((_ zero_extend 9) v2) v1)))
(let ((e52 (bvsge ((_ sign_extend 11) e8) v3)))
(let ((e53 (= ((_ zero_extend 11) e17) e9)))
(let ((e54 (bvsle ((_ sign_extend 11) e12) e16)))
(let ((e55 (bvslt e15 ((_ zero_extend 11) v2))))
(let ((e56 (bvule v2 e17)))
(let ((e57 (bvugt ((_ zero_extend 9) v2) e13)))
(let ((e58 (xor e47 e50)))
(let ((e59 (not e26)))
(let ((e60 (= e51 e44)))
(let ((e61 (= e37 e36)))
(let ((e62 (not e29)))
(let ((e63 (ite e41 e30 e32)))
(let ((e64 (= e40 e46)))
(let ((e65 (xor e55 e35)))
(let ((e66 (= e60 e59)))
(let ((e67 (ite e62 e38 e19)))
(let ((e68 (ite e34 e61 e66)))
(let ((e69 (and e27 e43)))
(let ((e70 (and e53 e48)))
(let ((e71 (xor e25 e69)))
(let ((e72 (not e31)))
(let ((e73 (and e72 e65)))
(let ((e74 (=> e71 e54)))
(let ((e75 (=> e42 e58)))
(let ((e76 (= e33 e56)))
(let ((e77 (= e45 e49)))
(let ((e78 (not e39)))
(let ((e79 (= e63 e28)))
(let ((e80 (or e52 e75)))
(let ((e81 (not e57)))
(let ((e82 (ite e22 e78 e79)))
(let ((e83 (not e68)))
(let ((e84 (and e82 e83)))
(let ((e85 (or e77 e20)))
(let ((e86 (and e24 e76)))
(let ((e87 (=> e23 e74)))
(let ((e88 (xor e67 e67)))
(let ((e89 (xor e64 e21)))
(let ((e90 (not e73)))
(let ((e91 (ite e70 e90 e88)))
(let ((e92 (xor e81 e91)))
(let ((e93 (=> e80 e80)))
(let ((e94 (not e86)))
(let ((e95 (not e84)))
(let ((e96 (xor e92 e94)))
(let ((e97 (=> e93 e96)))
(let ((e98 (ite e97 e89 e89)))
(let ((e99 (not e87)))
(let ((e100 (and e98 e85)))
(let ((e101 (=> e100 e100)))
(let ((e102 (or e99 e99)))
(let ((e103 (and e95 e101)))
(let ((e104 (= e103 e103)))
(let ((e105 (or e104 e104)))
(let ((e106 (= e105 e102)))
e106
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)


(reset)
(set-option :auto-config false)
(set-option :rewriter.hi-div0 false)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 8) (_ BitVec 6) (_ BitVec 2)) (_ BitVec 7))
(declare-fun p0 ( (_ BitVec 2)) Bool)
(declare-fun v0 () (_ BitVec 15))
(declare-fun v1 () (_ BitVec 10))
(declare-fun v2 () (_ BitVec 1))
(declare-fun v3 () (_ BitVec 12))
(assert (let ((e4(_ bv39 7)))
(let ((e5 (f0 ((_ sign_extend 7) v2) ((_ sign_extend 5) v2) ((_ zero_extend 1) v2))))
(let ((e6 (ite (p0 ((_ extract 6 5) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e7 (bvurem ((_ zero_extend 11) e6) v3)))
(let ((e8 ((_ rotate_left 0) v2)))
(let ((e9 (bvxor ((_ zero_extend 5) e5) v3)))
(let ((e10 (bvlshr ((_ sign_extend 6) v2) e5)))
(let ((e11 (ite (bvslt e5 ((_ sign_extend 6) e6)) (_ bv1 1) (_ bv0 1))))
(let ((e12 (ite (bvsgt ((_ sign_extend 8) e10) v0) (_ bv1 1) (_ bv0 1))))
(let ((e13 (bvor v1 ((_ sign_extend 9) e11))))
(let ((e14 (bvshl v0 ((_ zero_extend 3) e9))))
(let ((e15 (bvadd ((_ zero_extend 2) e13) e7)))
(let ((e16 (bvurem ((_ zero_extend 11) v2) e15)))
(let ((e17 (ite (bvslt v0 ((_ sign_extend 3) e9)) (_ bv1 1) (_ bv0 1))))
(let ((e18 (ite (bvuge e5 e4) (_ bv1 1) (_ bv0 1))))
(let ((e19 (p0 ((_ extract 6 5) e10))))
(let ((e20 (bvuge ((_ zero_extend 5) v1) v0)))
(let ((e21 (bvslt e16 ((_ sign_extend 5) e10))))
(let ((e22 (bvsgt ((_ sign_extend 5) e10) e16)))
(let ((e23 (bvsle ((_ zero_extend 11) e8) e7)))
(let ((e24 (= ((_ zero_extend 5) e10) e7)))
(let ((e25 (bvuge ((_ sign_extend 6) e18) e4)))
(let ((e26 (distinct v3 ((_ zero_extend 2) v1))))
(let ((e27 (bvule e6 e17)))
(let ((e28 (p0 ((_ sign_extend 1) e6))))
(let ((e29 (bvuge ((_ sign_extend 6) e18) e5)))
(let ((e30 (bvuge e8 e6)))
(let ((e31 (distinct e15 ((_ sign_extend 11) e11))))
(let ((e32 (bvule ((_ sign_extend 11) e6) e16)))
(let ((e33 (bvule ((_ zero_extend 6) e11) e4)))
(let ((e34 (bvsle v3 v3)))
(let ((e35 (bvsgt ((_ zero_extend 11) e6) e16)))
(let ((e36 (bvule ((_ sign_extend 11) e11) v3)))
(let ((e37 (bvuge e14 ((_ zero_extend 3) e16))))
(let ((e38 (= ((_ sign_extend 3) e15) v0)))
(let ((e39 (bvsgt e11 e11)))
(let ((e40 (bvsge e18 e18)))
(let ((e41 (distinct e17 e11)))
(let ((e42 (p0 ((_ extract 4 3) e10))))
(let ((e43 (p0 ((_ extract 1 0) e10))))
(let ((e44 (bvult v0 ((_ zero_extend 14) e18))))
(let ((e45 (p0 ((_ extract 10 9) v3))))
(let ((e46 (bvuge e9 ((_ zero_extend 5) e10))))
(let ((e47 (bvsge v3 ((_ sign_extend 11) e6))))
(let ((e48 (bvslt v3 ((_ sign_extend 5) e4))))
(let ((e49 (bvsge e18 e17)))
(let ((e50 (bvult e15 ((_ sign_extend 5) e10))))
(let ((e51 (bvslt ((_ zero_extend 9) v2) v1)))
(let ((e52 (bvsge ((_ sign_extend 11) e8) v3)))
(let ((e53 (= ((_ zero_extend 11) e17) e9)))
(let ((e54 (bvsle ((_ sign_extend 11) e12) e16)))
(let ((e55 (bvslt e15 ((_ zero_extend 11) v2))))
(let ((e56 (bvule v2 e17)))
(let ((e57 (bvugt ((_ zero_extend 9) v2) e13)))
(let ((e58 (xor e47 e50)))
(let ((e59 (not e26)))
(let ((e60 (= e51 e44)))
(let ((e61 (= e37 e36)))
(let ((e62 (not e29)))
(let ((e63 (ite e41 e30 e32)))
(let ((e64 (= e40 e46)))
(let ((e65 (xor e55 e35)))
(let ((e66 (= e60 e59)))
(let ((e67 (ite e62 e38 e19)))
(let ((e68 (ite e34 e61 e66)))
(let ((e69 (and e27 e43)))
(let ((e70 (and e53 e48)))
(let ((e71 (xor e25 e69)))
(let ((e72 (not e31)))
(let ((e73 (and e72 e65)))
(let ((e74 (=> e71 e54)))
(let ((e75 (=> e42 e58)))
(let ((e76 (= e33 e56)))
(let ((e77 (= e45 e49)))
(let ((e78 (not e39)))
(let ((e79 (= e63 e28)))
(let ((e80 (or e52 e75)))
(let ((e81 (not e57)))
(let ((e82 (ite e22 e78 e79)))
(let ((e83 (not e68)))
(let ((e84 (and e82 e83)))
(let ((e85 (or e77 e20)))
(let ((e86 (and e24 e76)))
(let ((e87 (=> e23 e74)))
(let ((e88 (xor e67 e67)))
(let ((e89 (xor e64 e21)))
(let ((e90 (not e73)))
(let ((e91 (ite e70 e90 e88)))
(let ((e92 (xor e81 e91)))
(let ((e93 (=> e80 e80)))
(let ((e94 (not e86)))
(let ((e95 (not e84)))
(let ((e96 (xor e92 e94)))
(let ((e97 (=> e93 e96)))
(let ((e98 (ite e97 e89 e89)))
(let ((e99 (not e87)))
(let ((e100 (and e98 e85)))
(let ((e101 (=> e100 e100)))
(let ((e102 (or e99 e99)))
(let ((e103 (and e95 e101)))
(let ((e104 (= e103 e103)))
(let ((e105 (or e104 e104)))
(let ((e106 (= e105 e102)))
e106
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
